(set-option :model_validate true)
(set-option :model true)
(set-option :smt.arith.eager_eq_axioms false)
(set-option :sat.force_cleanup false)
(set-option :sat.abce false)
(set-option :sat.branching.anti_exploration false)
(set-option :sat.bce true)
(set-option :sat.cut.npn3 false)
(set-option :model.inline_def false)
(set-option :nlsat.randomize false)
(set-option :smt.phase_selection 0)
(set-option :smt.threads 1)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const i0 Int)
(declare-const i1 Int)
(declare-const i2 Int)
(declare-const i4 Int)
(declare-const i6 Int)
(declare-const i7 Int)
(declare-const v16 Bool)
(declare-const i8 Int)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const v20 Bool)
(declare-const i9 Int)
(declare-const v21 Bool)
(declare-const v22 Bool)
(declare-const v23 Bool)
(declare-const v24 Bool)
(declare-const v25 Bool)
(declare-const i10 Int)
(declare-const v26 Bool)
(declare-const v27 Bool)
(declare-const i11 Int)
(declare-const v28 Bool)
(assert (or (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)) v20 v20))
(assert (or (and v2 v3) (=> v20 v7) v9))
(assert (or (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13))))
(assert (or (=> v15 v12) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)) (<= i6 (+ 63 i0 i4))))
(assert (or (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) v2 (<= 60 i6)))
(assert (or (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (=> v20 v7) (not v23)))
(assert (or (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) v9 v2))
(assert (or (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) v2 v9))
(assert (or v19 (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13)) v9))
(assert (or (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) v2 (not v23)))
(assert (or (and v2 v3) (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13)) v9))
(assert (or (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (=> v15 v10) (<= i6 (+ 63 i0 i4))))
(assert (or (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13)) (<= i6 (+ 63 i0 i4)) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))))
(assert (or (and v2 v3) (=> v20 v7) v9))
(assert (or v20 (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)) v8))
(assert (or (=> v15 v10) (=> v20 v7) (and v14 (>= (abs i6) i2) (or (distinct i2 i0) v8 v18) v2 v24 (>= (abs i6) i2) (=> v15 v10) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v26 v11)))
(assert (or v20 (<= 60 i6) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)))))
(assert (or (=> v15 v10) (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (=> v15 v12)))
(assert (or v2 (and v14 (>= (abs i6) i2) (or (distinct i2 i0) v8 v18) v2 v24 (>= (abs i6) i2) (=> v15 v10) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v26 v11) (<= 60 i6)))
(assert (or (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v20 (and v2 v3)))
(assert (or (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13)) (>= (abs i6) i2) v19))
(assert (or (=> v20 v7) (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) v9))
(assert (or (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13)) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12)))
(assert (or (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (not v23) (=> v15 v10)))
(assert (or (=> v15 v10) (<= i6 (+ 63 i0 i4)) v20))
(assert (or (<= 60 i6) v20 (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13))))
(assert (or v19 (=> v20 v7) (and v2 v3)))
(assert (or (=> v15 v10) (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) v8))
(assert (or v9 (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)) (=> v15 v12)))
(assert (or (and v14 (>= (abs i6) i2) (or (distinct i2 i0) v8 v18) v2 v24 (>= (abs i6) i2) (=> v15 v10) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v26 v11) v19 (and v14 (>= (abs i6) i2) (or (distinct i2 i0) v8 v18) v2 v24 (>= (abs i6) i2) (=> v15 v10) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v26 v11)))
(assert (or (and v14 (>= (abs i6) i2) (or (distinct i2 i0) v8 v18) v2 v24 (>= (abs i6) i2) (=> v15 v10) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v26 v11) v19 (=> v15 v12)))
(assert (or v20 v9 v9))
(assert (or (=> v20 v7) v8 (=> v15 v12)))
(assert (or (and v2 v3) v19 (<= 60 i6)))
(assert (or (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (>= (abs i6) i2) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))))
(assert (or (=> v20 v7) (=> v15 v12) (<= i6 (+ 63 i0 i4))))
(assert (or (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)) v20 (<= i6 (+ 63 i0 i4))))
(assert (or (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (=> v15 v12) v20))
(assert (or (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13)) (=> v20 v7) (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6)))
(assert (or (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) v2 v9))
(assert (or v19 (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13)) v2))
(assert (or (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v19 v2))
(assert (or v8 (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (and v14 (>= (abs i6) i2) (or (distinct i2 i0) v8 v18) v2 v24 (>= (abs i6) i2) (=> v15 v10) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v26 v11)))
(assert (or (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13)) (=> v15 v10) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12)))
(assert (or v9 v9 (and v2 v3)))
(assert (or v20 (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12)))
(assert (or v19 (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) (=> v20 v7)))
(assert (or v20 v8 (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)))))
(assert (or (=> v20 v7) (not v23) v19))
(assert (or (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v2 (not v23)))
(assert (or (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) (=> v15 v12) v9))
(assert (or (>= (abs i6) i2) v9 (and v14 (>= (abs i6) i2) (or (distinct i2 i0) v8 v18) v2 v24 (>= (abs i6) i2) (=> v15 v10) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v26 v11)))
(assert (or (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (not v23) v8))
(assert (or v9 (=> v15 v10) (not v23)))
(assert (or (and v14 (>= (abs i6) i2) (or (distinct i2 i0) v8 v18) v2 v24 (>= (abs i6) i2) (=> v15 v10) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v26 v11) v19 v19))
(assert (or v8 v9 (=> v15 v12)))
(assert (or (<= i6 (+ 63 i0 i4)) (=> v15 v10) v9))
(assert (or (=> v15 v10) (=> v20 v7) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12)))
(assert (or (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v9 v20))
(assert (or (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) v20 (=> v15 v10)))
(assert (or v9 (and v14 (>= (abs i6) i2) (or (distinct i2 i0) v8 v18) v2 v24 (>= (abs i6) i2) (=> v15 v10) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v26 v11) v20))
(assert (or (not v23) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)) v19))
(assert (or (=> v15 v12) v20 v9))
(assert (or v9 (=> v15 v10) v2))
(assert (or (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12)))
(assert (or (>= (abs i6) i2) (<= 60 i6) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)))))
(assert (or v8 (>= (abs i6) i2) (<= 60 i6)))
(assert (or (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (=> v15 v10) (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6)))
(assert (or (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)) (and v2 v3)))
(assert (or (and v14 (>= (abs i6) i2) (or (distinct i2 i0) v8 v18) v2 v24 (>= (abs i6) i2) (=> v15 v10) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v26 v11) (<= 60 i6) (not v23)))
(assert (or (<= 60 i6) (=> v15 v10) (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6)))
(assert (or (=> v15 v10) v20 (<= i6 (+ 63 i0 i4))))
(assert (or (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (=> v20 v7) v9))
(assert (or (not v23) (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13)) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))))
(assert (or v20 (=> v15 v10) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)))))
(assert (or v2 v20 (<= 60 i6)))
(assert (or (and v14 (>= (abs i6) i2) (or (distinct i2 i0) v8 v18) v2 v24 (>= (abs i6) i2) (=> v15 v10) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v26 v11) (not v23) (<= 60 i6)))
(assert (or v2 (=> v20 v7) v19))
(assert (or (<= i6 (+ 63 i0 i4)) v19 (=> v15 v12)))
(assert (or (<= i6 (+ 63 i0 i4)) v20 (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6)))
(assert (or v9 (and v2 v3) (=> v15 v12)))
(assert (or (not v23) (=> v15 v10) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12)))
(assert (or (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)) (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13)) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12)))
(assert (or (=> v15 v10) (=> v20 v7) v19))
(assert (or v8 v9 v20))
(assert (or (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)) v19 v19))
(assert (or v8 (and v14 (>= (abs i6) i2) (or (distinct i2 i0) v8 v18) v2 v24 (>= (abs i6) i2) (=> v15 v10) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v26 v11) (<= 60 i6)))
(assert (or (and v2 v3) v2 (=> v15 v10)))
(assert (or (=> v15 v12) (not v23) (<= 60 i6)))
(assert (or (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (=> v15 v10)))
(assert (or v19 v9 (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13))))
(assert (or (<= 60 i6) (>= (abs i6) i2) v9))
(assert (or (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13)) (not v23) (=> v15 v10)))
(assert (or (and v2 v3) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) v19))
(assert (or (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v19 (=> v15 v12)))
(assert (or (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13)) v20 v19))
(assert (or (<= 60 i6) v20 (=> v15 v12)))
(assert (or (=> v20 v7) (=> v20 v7) (<= 60 i6)))
(assert (or (=> v20 v7) v9 (not v23)))
(assert (or (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)) (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13)) (>= (abs i6) i2)))
(assert (or (and v2 v3) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (and v2 v3)))
(assert (or (=> v20 v7) v9 (and v2 v3)))
(assert (or v9 (=> v15 v10) v20))
(assert (or (=> v20 v7) v19 (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)))))
(assert (or (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)) v19 v20))
(assert (or (=> v15 v10) v2 (and v14 (>= (abs i6) i2) (or (distinct i2 i0) v8 v18) v2 v24 (>= (abs i6) i2) (=> v15 v10) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v26 v11)))
(assert (or (<= 60 i6) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (>= (abs i6) i2)))
(assert (or (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13)) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v9))
(assert (or (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) v19 (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12)))
(assert (or v2 (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (and v14 (>= (abs i6) i2) (or (distinct i2 i0) v8 v18) v2 v24 (>= (abs i6) i2) (=> v15 v10) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v26 v11)))
(assert (or (and v14 (>= (abs i6) i2) (or (distinct i2 i0) v8 v18) v2 v24 (>= (abs i6) i2) (=> v15 v10) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v26 v11) v20 (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))))
(assert (or (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)) (=> v15 v12)))
(assert (or v9 (=> v15 v12) (<= i6 (+ 63 i0 i4))))
(assert (or (and v14 (>= (abs i6) i2) (or (distinct i2 i0) v8 v18) v2 v24 (>= (abs i6) i2) (=> v15 v10) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v26 v11) v8 (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6)))
(assert (or v8 (=> v15 v12) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))))
(assert (or (and v14 (>= (abs i6) i2) (or (distinct i2 i0) v8 v18) v2 v24 (>= (abs i6) i2) (=> v15 v10) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v26 v11) v8 (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12)))
(assert (or v9 (and v2 v3) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)))))
(assert (or (<= 60 i6) (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13)) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))))
(assert (or (<= 60 i6) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)) v9))
(assert (or v8 (=> v15 v12) (not v23)))
(assert (or (=> v15 v10) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6)) (=> v15 v12)))
(assert (or (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) v2 (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13))))
(assert (or (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v19 (=> v20 v7)))
(assert (or v8 (=> v15 v12) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12)))
(assert (or (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) v8 (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))))
(assert (or v2 (=> v20 v7) (not v23)))
(assert (or (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (=> v15 v10) v2))
(assert (or v2 (=> v15 v10) v9))
(assert (or (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) (=> v15 v12) (>= (abs i6) i2)))
(assert (or (=> v20 v7) v2 (and v14 (>= (abs i6) i2) (or (distinct i2 i0) v8 v18) v2 v24 (>= (abs i6) i2) (=> v15 v10) (=> (or (distinct i2 i0) v8 v18) (=> (xor v14 v8 v15 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v5 v5 v2 v8 (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13) v14 v6) (<= 60 i6))) (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v26 v11)))
(assert (or (distinct v3 v12 v14 v1 v6 v4 (distinct i7 (abs i6)) v12 (distinct i7 (abs i6)) v12) v9 (or (=> v15 v10) (or (distinct i2 i0) v8 v18) v13 v14 v10 (<= i6 (+ 63 i0 i4)) (>= (abs i6) i2) (xor v14 v11 v15 v10 v15 v13 v11 v8 v1 v13))))
(assert (or v8 (>= (abs i6) i2) v8))
(assert (or (<= 60 i6) v8 (=> v15 v12)))
(check-sat)
(exit)
